% Chapter 4

\chapter{Traducción de problemas PH}
\label{Chapter3}
\lhead{Capítulo 3. \emph{Traducción de problemas PH}}

%In this approach, a decision problem $\Pi$ in NP is encoded as a
%second-order existential (\SOE) formula $\Phi$ while a particular
%instance is encoded as first-order structure $\A$ in a way that
%$\A\models\Phi$ iff the instance encoded by $\A$ satisfies belongs to $\Pi$.
%This is a general and feasible idea as it is known that \SOE
%captures the class NP \cite{immerman:book}.
%The pair $\tup{\Phi,\A}$ is then fed into a (software) tool that
%outputs a \STRIPS problem $P$ that has a solution (plan) iff $\A\models\Phi$,
%thus allowing the utilization of the current planning technology
%to automatically solve the problems in NP that are expressed as
%second-order formulas.
%Moreover, the problem $P$ is not an arbitrary \STRIPS problem but
%one that can be solved in polytime by a non-deterministic
%Turing machine, thus guaranteeing that the whole approach is not
%an overkill from the standpoint of complexity theory.
%Furthermore, the function $\tup{\Phi,\cdot}:\struc\mapsto\STRIPS$ 
%that is implemented by the tool for fixed $\Phi$ and that maps
%first-order structures $\A$ into \STRIPS problems $P$ is computable
%in polynomial time and thus corresponds to a genuine \emph{polytime many-one reduction}
%from $\Pi$ into \STRIPS.

%Since it is known that other (bigger) complexity classes are also
%captured in second-order logic, PMB left as an open issue the
%development of a tool capable of targeting such classes.
Este capítulo describe la extensión de la herramienta desarrollada en este
trabajo para la traducción de problemas de decisión pertenecientes a la clase de
complejidad de la jerarquía polinomial, PH, los cuales son capturados por la lógica de
segundo orden. En primer lugar se habla brevemente sobre la complejidad de esta
clase de problemas. Luego se presenta, mediante ejemplos, una traducción alternativa a la
expuesta en el capítulo anterior que permite traducir cualquier problema
expresado en lógica general de segundo orden a un problema de planificación
automática.

\section{Complejidad}

Al contrario que en el caso de NP,
esta vez no se ofrecen garantías de complejidad sobre la extensión de la
reducción: los problemas \STRIPS generados por ella en general no serán
solucionables en tiempo polinomial no determinístico.
Esto se debe a que los problemas de esta clase sólo admiten planes
de longitud exponencial en el peor caso ya que PH contiene, además de a NP, las
clases coNP y $\Sigma^p_k$ para todo $k\geq 1$. La clase $\Sigma_p^2$, por
ejemplo, es igual a $NP^{NP}$, la clase de problemas resolubles en tiempo
polinomial no determinístico contando un oráculo para resolver problemas NP.

Una característica de NP es la 
disponibilidad de un \textit{certificado} que valida en tiempo polinomial una
respuesta al problema de decisión: tal garantía no es ofrecida en estas clases
superiores.
De este modo, los problemas de planificación que produce la reducción son
cortos, pues pueden ser codificados por las traducciones de estructuras finitas
$\A$, pero sus soluciones son, potencialmente, muy largas.

%The consequences of having small problems with long solutions
%are several. Among others, such problems pose a difficult
%challenge on the current state-of-the-art planners which are
%all based on heuristic search. In particular, heuristics functions
%that are based on the delete relaxation or that do not take into
%account that the same action may be applied a large (i.e., exponential)
%number of times will probably fail at being effective for guiding
%the search.
%Surprisingly, the current best SAT-based planner, the planner M,
%is able to solve some of these challenging
%\STRIPS problems for which forward-search planners like LAMA'11
%are totally lost. Yet, more surprisingly, LAMA'11 is quite
%superior to M in one of the tested domains (more about this below).

%\section{Capturing \PH in Second-Order Logic}
%
%NP is captured by \SOE \cite{fagin:spectra}.
%This result means that any decision problem $\Pi$ in NP can be
%characterized by a second-order formula $\Phi$ that looks like
%\begin{equation}
%\label{eq:soe}
%\Phi = (\exists R_1^{a_1})\cdots(\exists R_n^{a_n})\psi
%\end{equation}
%where each symbol $R_i^{a_i}$ is a existentially-quantified relation
%of arity $a_i$, and $\psi$ is an arbitrary first-order sentence 
%over a vocabulary containing $\{R_1^{a_1},\ldots,R_n^{a_n}\}$.
%That is, $\Pi$ is the set of instances (words in a language)
%that when encoded as structures $\A$ satisfy the formula $\Phi$.

coNP es la clase complementaria a NP, y es capturada por la lógica \SOA\ 
que contiene fórmulas que se apegan a la Ecuación \ref{eq:soa}:
\begin{equation}
\label{eq:soa}
\Phi = (\forall R_1^{a_1})\cdots(\forall R_n^{a_n})\psi
\end{equation}

En general, $\Sigma^p_k$ es capturada por fórmulas cuya estructura contiene $k$
bloques alternantes de cuantificadores, empezando con los existenciales. Por
ejemplo, $\Sigma^p_2=\SOEA$ corresponde a fórmulas de la forma:
\begin{equation}
\Phi = (\exists R_1^{a_1}) \cdots (\exists R_n^{a_n}) 
       (\forall S_1^{a'_1}) \cdots (\forall S_m^{a'_m})
       \psi
\end{equation}

%Como \PH $ = \bigcup_{k\geq 1}\Sigma^p_k$ y es caracterizada por fórmulas
%arbitrarias de lógica de segundo orden \cite{immerman:book}, la extensión
%deberá manejar estas fórmulas
%
%the extended tool we sought must target such formulas
%instead of the more restricted \SOE formulas.
%On the other hand, we know that $\PH\subseteq\PSPACE$, the
%decision problem for \STRIPS is \PSPACE-complete and there
%are no known syntactic restrictions on \STRIPS that place
%its decision problem in \PH. Thus, the new tool will focus
%on generating (unrestricted) \STRIPS problems.

Considere ahora la fórmula $\Phi=(\forall R^1)\psi$
y una estructura $\A$ con universo $|\A|$.
Se dice que $\Phi$ es válida en $\A$ si y sólo si para toda
interpretación $R^\A$ de $R$, donde $R^\A \subseteq |\A|$, se tiene
$\tup{\A,R^\A}\models\psi$. Como existen $2^{\|\A\|}$ interpretaciones
distintas de $R$, una demostración de $\A\models\Phi$ puede ser de
\textbf{tamaño exponencial}. Por ejemplo, si $\Phi_{\UNSAT}$ denota el problema
complementario a satisfacibilidad proposicional, entonces una prueba de que la
estructura $\A$ es no satisfacible es de tamaño exponencial, dado que debe
considerar todos los valores de verdad para las variables proposicionales de
$\A$. Por ello, las soluciones para el problema de planificación $P$ generado
por el par $\tup{\Phi_\UNSAT,\A}$ codifican tales pruebas y son de tamaño
exponencial.

\section{Traducción a \STRIPS}

\subsection{Sistema de tipos}
Antes de extender la traducción a \PH es conveniente agregarle un sistema
sencillo de tipos.

Sea $\t^*$ un sistema, creado a partir de un conjunto finito 
$\t=\{\mathbf{t}_0,\mathbf{t}_1,\ldots,\mathbf{t}_N\}$
de \textbf{tipos atómicos}, donde $\t^*$ es el conjunto más pequeño que
contiene $t$ y todos los tipos de la forma $t=t'\times t''$
para $t'\in\t^*$ y $t''\in\t$.

La idea es que a cada objeto en una estructura de primer orden le es asignado
un tipo atómico, siendo $\mathbf{t}_0$ el tipo que contiene a todos los
objetos.
Los tipos se utilizan para restringir las iteraciones sobre las
cuantificaciones de primer y segundo orden en las fórmulas.
Por ejemplo, $(\forall x\in t)$ se refiere a una cuantificación de primer orden
sobre todos los objetos de tipo $t\in\t$, mientras que
$(\forall R^t)$ se refiere a un predicado de segundo orden universalmente
cuantificado $R$ de tipo $t\in\t^*$.
La única restriccion que se exige es que los tipos complejos en 
$\t^*\setminus\t$ sólo aparezcan en cuantificaciones de segundo orden.

Considere una fórmula general \LSO\ de la forma
\begin{equation}
\Phi = (\Q_1R_1^{t_1})(\Q_2R_2^{t_2})\cdots(\Q_nR_n^{t_n})\psi
\end{equation}
donde cada $\Q_i\in\{\exists,\forall\}$ es un cuantificador de segundo orden,
$R_i$ es un símbolo relacional de tipo $t_i\in\t^*$,
y $\psi$ es una sentencia de primer orden.

Sea $\A$ una estructura de primer orden en $\struc[\sigma]$.
Se muestra cómo generar un problema de planificación $P$ que tiene solución si
y sólo si $\A\models\Phi$.
%Further, let $\A$ be a first-order structure over the
%vocabulary of $\psi$.

Según la traducción descrita en el capítulo 2, 
$P$ tiene condiciones de la forma $\FT[\theta]$
para cada subfórmula $\theta$ de $\psi$ y con parámetros que corresponden a las
variables libres de $\theta$. Por ejemplo, si $\Phi$ es la fórmula para SAT:
\begin{alignat*}{1}
\Phi_\SAT &= (\exists T^\text{Var})\psi_\SAT \,, \\
\psi_\SAT &= (\forall y\in \text{Cls})(\exists x\in\text{Var}) \notag \\
          &\quad\quad\quad\quad
               [(P(x,y) \land T(x)) \lor (N(x,y) \lor \neg T(x))]
\end{alignat*}
donde `Var' y `Cls' son los tipos para variables y cláusulas,
entonces existe una condición $\FT[\theta]$ con parámetros
$\tup{x,y}$ para la subfórmula $\theta(x,y)=N(x,y)\lor\neg T(x)$.
En $\psi_\SAT$, las relaciones $P(x,y)$ y $N(x,y)$ denotan
que la variable $x$ aparece positiva o negativa, respectivamente, en la
cláusula $y$.
%the clause $y$; these relations are fixed for a given SAT instance
%and their interpretation is given in the structure $\A$ that
%encodes the instance.
%Por otro lado, la relación existencialmente cuantificada $T$ codifica 
%On the other hand, the existentially-quantified relation $T$
%encodes the sought model in a way that $T(x)$ is true iff the
%variable $x$ is assigned the truth-value true.

%The problem $P$ has actions for choosing the valuation $T$,
%that is represented by fluents of the form `$\texttt{T}(?x)$'
%and `$\texttt{not\_T}(?x)$', and actions for building a
%proof for $\psi_\SAT$ that are designed to work by following
%the recursive structure of $\psi_\SAT$.
%The goal of the problem is defined as the single fluent
%$\FT[\psi_\SAT]$ which has no parameters as $\psi_\SAT$
%is assumed to be a sentence.

%\smallskip

%In our approach, we make use of the same fluents that denote
%the validity of subformulas and the quantified relations.
\subsection{Traducción del operador \texttt{so-forall}}
Para la extensión de la herramienta, debe tenerse en cuenta cómo las relaciones
cuantificadas se construyen y se intercalan con las pruebas de las subfórmulas.
Este problema no surge con los problemas \SOE, debido a que hay una sola
interpretación que construir para cada fórmula existencialmente cuantificada,
pero para fórmulas generales es necesario construir e intentar probar varias
interpretaciones diferentes.
Para aclarar este punto, considere la fórmula para UNSAT, que contiene una
relación unaria $T$ cuantificada universalmente:

\begin{alignat*}{1}
\Phi_\UNSAT &= (\forall T^\text{Var})\psi_\UNSAT \\
\psi_\UNSAT &= (\exists y\in\text{Cls})(\forall x\in\text{Var}) \\
            &\quad\quad\ [(P(x,y) \land \neg T(x))\lor(N(x,y)\land T(x))\land NotIn(x,y)]
\end{alignat*}

Donde la relación $NotIn(x,y)$ indica que la variable $x$ no está presente en la cláusula $y$.

Esta fórmula expresa que para toda relación $T$ sobre variables
proposicionales, existe una cláusula $y$ tal que para cada variable $x$, o $x$
aparece positiva en $y$ y $x$ es falsa, o $x$ aparece negativa en $y$ y $x$ es
verdadera, o $x$ no aparece en $y$.
UNSAT se puede traducir automáticamente a \STRIPS considerando acciones que
\textbf{iteran} sobre todas las posibles relaciones $T$, y acciones para
obtener la condición $\FT[\psi_\UNSAT]$ para cada una de estas $T$.

Como $T$ es una relación unaria, hay $2^n$ relaciones distintas en $n$
variables. Cada relación puede ser codificada con una cadena binaria
de tamaño $n$ (un bit por variable) tal que el $i$-ésimo bit es 1 si y sólo si
la $i$-ésima variable $x_i$ pertenece a $T$. Luego, iterar sobre todas las
relaciones es equivalente a iterar sobre todas las cadenas binarias de tamaño
$n$: puede hacerse empezando con la relación vacía, que corresponde a
`0\ldots00', y sucesivamente ``sumando 1 a la cadena'' hasta llegar a `1\ldots11'.

La Figura \ref{fig:unsat} muestra 5 acciones que realizan la iteración en el
caso de $\Phi_\UNSAT$: estas
acciones utilizan como condiciones adicionales $\FT[\Phi_\UNSAT]$,
\texttt{necesita-}$\FT[\Phi_\UNSAT]$, `Marcador-T($x$)', `VarPrimera-T($x$)',
`VarSuc-T($x,y$)' y `VarÚlt-T($x$)'. Los últimos tres tipos de condición son
estáticos: se agregan al estado inicial e implementan un orden estático de los
objetos que se refieren a variables proposicionales.

Se describirá brevemente cómo funciona la iteración.
El estado inicial contiene las condiciones estáticas que definen a los tipos
Var y Cls, y las relaciones binarias 
$N(x,y)$ y $P(x,y)$, más la condición
\texttt{necesita-}$\FT[\Phi_\UNSAT]$. El estado final contiene solamente la
condición $\FT[\Phi_\UNSAT]$.
Inicialmente, la única acción aplicable es A1, que interpreta a $T$ como la
relación vacía y agrega la condición \texttt{necesita-}$\FT[\psi_\UNSAT]$.

Esta condición activa a las acciones para construir una prueba de $\psi_\UNSAT$
para el $T$ actual. Una vez que $\psi_\UNSAT$ ha sido probada, se agrega la
condición $\FT[\psi_\UNSAT]$.

Cuando $\psi_\UNSAT$ es demostrado, A2 se convierte en la única acción
aplicable y \textbf{borra la condición} $\FT[\psi_\UNSAT]$, agregando
Marcador($x$) para la primera variable en el orden estático.
Luego de A2, A3 debe ser aplicado, y cambia $T$ del modelo que corresponde a
0\ldots00 al modelo que corresponde a 0\ldots01. También agrega
\texttt{necesita-}$\FT[\psi_\UNSAT]$, lo que exige una demostración de
$\psi_\UNSAT$ para la nueva $T$.

La iteración procede de manera similar hasta demostrar $\psi_\UNSAT$ para el
útlimo modelo, que corresponde a 1\ldots11. Entonces, A5 es la única acción
aplicable y agrega $\FT[\Phi_\UNSAT]$, completando el plan.

\begin{figure}[t]
\centering
\fbox{
  %\resizebox{3.1in}{!}{
  \resizebox{!}{1.5in}{
    \begin{minipage}{3.6in}
    \begin{tabbing}
    Pre: \= \kill
    [A1] \textsc{ComenzarPrueba}: \\[.2em]
    Pre: \> \texttt{necesita-}$\FT[\Phi_\UNSAT]$ \\
    Efe: \> para cada $x\in\text{Var}$: no-T($x$) \,, \\
         \> $\neg$\texttt{necesita-}$\FT[\Phi_\UNSAT]$ \,,\, \texttt{necesita-}$\FT[\psi_\UNSAT]$ \\[1em]
    %%%
    [A2] \textsc{PrimeraIteración}($x$): \\[.2em]
    Pre: \> $\FT[\psi_\UNSAT]$ \,,\, VarPrimera-T($x$) \\
    Efe: \> $\neg$$\FT[\psi_\UNSAT]$ \,,\, Marcador-T($x$) \\[1em]
    %%%
    [A3] \textsc{SiguienteSobreExcluidos}($x$): \\[.2em]
    Pre: \> Marcador-T($x$) \,,\, no-T($x$) \\
    Efe: \> $\neg$no-T($x$) \,,\, T($x$) \,,\, $\neg$Marcador-T($x$) \,,\, \texttt{necesita-}$\FT[\psi_\UNSAT]$ \\[1em]
    %%%
    [A4] \textsc{SiguienteSobreIncluidos}($x,y$): \\[.2em]
    Pre: \> Marcador-T($x$) \,,\, T($x$) \,,\, VarSuc-T($x,y$) \\
    Efe: \> $\neg$T($x$) \,,\, no-T($x$) \,,\, $\neg$Marcador-T($x$) \,,\, Marcador-T($y$) \\[1em]
    %%%
    [A5] \textsc{TerminarPrueba}($x$): \\[.2em]
    Pre: Marcador-T($x$) \,,\, T($x$) \,,\, VarÚlt-T($x$) \\
    Efe: $\neg$T($x$) \,,\, no-T($x$) \,,\, $\neg$Marcador-T($x$) \,,\, $\FT[\Phi_\UNSAT]$
    \end{tabbing}
    \end{minipage}
  }
}
\caption[Acciones para realizar la iteración del cuantificador universal de
segundo orden]{Acciones para iterar sobre las $2^n$ relaciones unarias $T$
  que codifican las $2^n$ asignaciones de verdad para las $n$ variables
proposicionales de UNSAT.}
\label{fig:unsat}
\end{figure}

Nótese que este método de iteración es extensible a relaciones de aridad $k>1$.
El único cambio que se necesita es reemplazar $x$ y $y$ por $k$-tuplas de
variables. De igual forma, las condiciones que implementan el orden estático
deben reemplazarse por condiciones que implementen un orden estático sobre
$k$-tuplas.

\subsection{Traducción del operador \texttt{so-exists}}
Para garantizar la interoperabilidad con la traducción que se ha presentado arriba
para cuantificadores universales de segundo orden, y asegurar la posibilidad de anidar
cuantificadores existenciales y universales a fin de capturar PH,
debe modificarse ligeramente la traducción del operador existencial de segundo orden.

Concretamente, se mostrará la nueva traducción para el caso de SAT.
La Figura \ref{fig:sat} muestra las acciones que llevan a
cabo tal traducción.
Las traducciones de SAT y UNSAT comparten un mismo protocolo que controla
cuáles operadores se activan o desactivan dependiendo de qué parte de la
fórmula está siendo demostrada.

Por ejemplo, una fórmula en $\Sigma^p_2$ de la forma
$\Phi=(\exists T^{t_1})(\forall R^{t_2})\psi$ puede ser analizada como
\begin{equation}
\Phi = (\exists T^{t_1})\Psi \quad\text{con}\quad \Psi = (\forall R^{t_2})\psi
\end{equation}
de modo que las acciones de cuantificadores existenciales (parecidas a las de
SAT) puedan ser combinadas acciones de cuantificadores universales (parecidas a
las de UNSAT). Para realizar la combinación, el operador E5 (ver Figura
\ref{fig:sat}) del existencial de
segundo orden interno debe borrar las condiciones de todas las subfórmulas para
tener un ``estado limpio'' para la siguiente prueba.
%having fluents for the SO formula $\Phi_\SAT$ and by ``passing control''
%to the actions
%that prove $\FT[\psi_\SAT]$ in a way similar to UNSAT;

%The translations for SAT and UNSAT share a common protocol
%that controls which operators become active or inactive
%depending on which part of the formula is being proved.
%This protocol is designed to allow the composition of
%the two types of SO quantifiers, and thus to make a
%translation for \PH.

\begin{figure}[t]
\centering
\fbox{
  \resizebox{!}{1.5in}{
    \begin{minipage}{3.6in}
    \begin{tabbing}
    Pre: \= \kill
    [E1] \textsc{ComenzarPrueba}: \\[.2em]
    Pre: \> \texttt{necesita-}$\FT[\Phi_\SAT]$ \\
    Efe: \> para cada $x\in\text{Var}$: no-T($x$) \,,\,
$\neg$\texttt{necesita-}$\FT[\Phi_\SAT]$ \,,\, conjetura-T \\[1em]
    %%%
    [E2] \textsc{ColocarVerdadera}($x$): \\[.2em]
    Pre: \> conjetura-T\\
    Efe: T($x$) \,,\, $\neg$no-T($x$) \\[1em]
    %%%
    [E3] \textsc{ColocarFalsa}($x$): \\[.2em]
    Pre: \> conjetura-T\\
    Efe: no-T($x$) \,,\, $\neg$T($x$) \\[1em]
    %%%
    [E4] \textsc{ProbarSubfórmula}: \\[.2em]
    Pre: \> conjetura-T\\
    Efe: $\neg$conjetura-T \,,\, \texttt{necesita-}$\FT[\psi_\SAT]$ \\[1em]
    %%%
    [E5] \textsc{TerminarPrueba}: \\
    Pre: \> $\FT[\psi_\SAT]$\\
    Efe: $\neg$$\FT[\psi_\SAT]$ \,,\, $\FT[\Phi_\SAT]$
    \end{tabbing}
    \end{minipage}
  }
}
\caption{Acciones que implementan la nueva traducción para el cuantificador
existencial en SAT.}
\label{fig:sat}
\end{figure}
